(declare-fun i1 () Int)
(declare-fun seq3 () (Seq Int))
(declare-fun str2 () String)
(declare-fun str5 () String)
(declare-fun i4 () Int)
(push)
(assert (seq.contains seq3 (seq.unit (+ i4 (- i1 i4)))))
(assert (= str2 (str.substr str5 1 (- i1 i4))))
(check-sat)
